﻿// Jinx AJAX Framework
// Copyright (C) 2008 Blake Hegerle
//
// This program is free software: you can redistribute it and/or modify
// it under the terms of the GNU General Public License as published by
// the Free Software Foundation, either version 3 of the License, or
// (at your option) any later version.
//
// This program is distributed in the hope that it will be useful,
// but WITHOUT ANY WARRANTY; without even the implied warranty of
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
// GNU General Public License for more details.
//
// You should have received a copy of the GNU General Public License
// along with this program.  If not, see <http://www.gnu.org/licenses/>.

using System.IO;
using Core.Parsing;
using Core.Parsing.ContextFree;
using Core.Parsing.ContextFree.LR;
using Core.Parsing.LexicalAnalysis;

namespace Formality.FormalSystem.Parser
{
    public class PropositionParser
    {
        private static PropositionParser instance;
        public readonly UnaryOperators Binders;
        public readonly Grammar<Proposition> Grammar;
        public readonly LexerBuilder LexerBuilder;
        public readonly IParser<Proposition> Parser;
        public readonly PrecedenceRules PrecedenceRules;
        public readonly Terminals Terminals;
        public readonly UnaryOperators UnaryOperators;
        public bool Trace;

        private PropositionParser()
        {
            PrecedenceRules = new PrecedenceRules();
            UnaryOperators = new UnaryOperators();
            Binders = new UnaryOperators();
            Terminals = new Terminals();

            PrecedenceRules.Add(Operators.DEFINED, ":=");
            PrecedenceRules.Add(Operators.RULE);
            PrecedenceRules.Add(Operators.EQ, "==");
            PrecedenceRules.Add(Operators.EQUALS);
            PrecedenceRules.Add(Operators.NOT_EQUALS, "!=");
            PrecedenceRules.Add(Operators.IMPLIES, "->", '\u001a');
            PrecedenceRules.Add(Operators.OR, "|");
            PrecedenceRules.Add(Operators.AND, "&");

            UnaryOperators.Add(Operators.NOT, "~");
            UnaryOperators.Add(Operators.AXIOM);

            Binders.Add(Operators.FOR_ALL, "@");
            Binders.Add(Operators.EXISTS, "#");
            Binders.Add(Operators.LAMBDA, "\\");

            LexerBuilder = new GrammarLexer(Terminals, PrecedenceRules, Binders, UnaryOperators);

            Grammar = new GrammarBuilder(Terminals, PrecedenceRules).Grammar;

            Parser = new ParserFactory<Proposition>(Grammar).MakeParser();
        }

        public static PropositionParser Instance
        {
            get
            {
                if (instance == null)
                    instance = new PropositionParser();
                return instance;
            }
        }

        public Proposition Parse(TextReader Reader)
        {
            return Parser.Parse(LexerBuilder.NewLexer(Reader)).Bind();
        }

        public Proposition Parse(string Input)
        {
            return Parse(new StringReader(Input));
        }
    }
}